es:ES, dom:(E).
(e:E. (isrcv(e))  (((dom(sender(e)))))  (isrcv(sender(e))))
 (e:E. (isrcv(e))  (sub-es-sender(es;dom;e)  {e:E| (dom(e))} )) 

latex

Definitions	x:A. B(x), b, t  T, A, b, s = t, , , P  Q, sender(e), f(a), x:AB(x), x:A  B(x), P & Q, P  Q, Unit, left + right, isrcv(e), sub-es-sender(es;dom;e), E, {x:A| B(x)} , , #$n, A  B, , a < b, False, True, T, (e < e'), x:A. B(x), SWellFounded(R(x;y)), Type, ES, i  j , -n, n+m, n - m, Void, if b then t else f fi , t.1, case b of inl(x) => s(x) | inr(y) => t(y)
Lemmas	es-sender-causl, true wf, false wf, ge wf, nat properties, event system wf, es-E wf, es-causl-swellfnd, nat wf, es-causl wf, le wf, es-isrcv wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, es-sender wf, bool wf, bnot wf, not wf, assert wf